Issue783a.agda:3,7-8
Not in scope:
  Y
  at Issue783a.agda:3,7-8
when scope checking Y
